YES 6.849
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ BR
mainModule Main
| ((rangeSize :: (Int,Int) -> Int) :: (Int,Int) -> Int) |
module Main where
Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern
r@(vv,vw)
is replaced by the following term
(vv,vw)
The bind variable of the following binding Pattern
b@(wu,wv)
is replaced by the following term
(wu,wv)
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Main
| ((rangeSize :: (Int,Int) -> Int) :: (Int,Int) -> Int) |
module Main where
Cond Reductions:
The following Function with conditions
rangeSize | (vv,vw) |
| | null (range (vv,vw)) | |
| | otherwise | |
|
is transformed to
rangeSize | (vv,vw) | = rangeSize2 (vv,vw) |
rangeSize1 | vv vw True | = 0 |
rangeSize1 | vv vw False | = rangeSize0 vv vw otherwise |
rangeSize0 | vv vw True | = index (vv,vw) vw + 1 |
rangeSize2 | (vv,vw) | = rangeSize1 vv vw (null (range (vv,vw))) |
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
The following Function with conditions
takeWhile | p [] | = [] |
takeWhile | p (x : xs) | |
is transformed to
takeWhile | p [] | = takeWhile3 p [] |
takeWhile | p (x : xs) | = takeWhile2 p (x : xs) |
takeWhile1 | p x xs True | = x : takeWhile p xs |
takeWhile1 | p x xs False | = takeWhile0 p x xs otherwise |
takeWhile0 | p x xs True | = [] |
takeWhile2 | p (x : xs) | = takeWhile1 p x xs (p x) |
takeWhile3 | p [] | = [] |
takeWhile3 | xu xv | = takeWhile2 xu xv |
The following Function with conditions
index | (wu,wv) i |
| | inRange (wu,wv) i | |
| | otherwise | |
|
is transformed to
index | (wu,wv) i | = index2 (wu,wv) i |
index0 | wu wv i True | = error [] |
index1 | wu wv i True | = i - wu |
index1 | wu wv i False | = index0 wu wv i otherwise |
index2 | (wu,wv) i | = index1 wu wv i (inRange (wu,wv) i) |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
mainModule Main
| ((rangeSize :: (Int,Int) -> Int) :: (Int,Int) -> Int) |
module Main where
Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
mainModule Main
| (rangeSize :: (Int,Int) -> Int) |
module Main where
Haskell To QDPs
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(xx630), Succ(xx620)) → new_primPlusNat(xx630, xx620)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(xx630), Succ(xx620)) → new_primPlusNat(xx630, xx620)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusInt(xx66, Succ(xx670)) → new_primPlusInt(xx66, xx670)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusInt(xx66, Succ(xx670)) → new_primPlusInt(xx66, xx670)
The graph contains the following edges 1 >= 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusInt0(xx62, xx63, Succ(xx640)) → new_primPlusInt0(xx62, xx63, xx640)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusInt0(xx62, xx63, Succ(xx640)) → new_primPlusInt0(xx62, xx63, xx640)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusInt1(xx69, Succ(xx700)) → new_primPlusInt1(xx69, xx700)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusInt1(xx69, Succ(xx700)) → new_primPlusInt1(xx69, xx700)
The graph contains the following edges 1 >= 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusInt2(Succ(xx1220), Succ(xx1210)) → new_primPlusInt2(xx1220, xx1210)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusInt2(Succ(xx1220), Succ(xx1210)) → new_primPlusInt2(xx1220, xx1210)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusInt3(xx125, xx126, Succ(xx1270)) → new_primPlusInt3(xx125, xx126, xx1270)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusInt3(xx125, xx126, Succ(xx1270)) → new_primPlusInt3(xx125, xx126, xx1270)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusInt4(xx121, xx122, Succ(xx1230)) → new_primPlusInt4(xx121, xx122, xx1230)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusInt4(xx121, xx122, Succ(xx1230)) → new_primPlusInt4(xx121, xx122, xx1230)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusInt5(xx113, xx114, Succ(xx1150), Succ(xx1160)) → new_primPlusInt5(xx113, xx114, xx1150, xx1160)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusInt5(xx113, xx114, Succ(xx1150), Succ(xx1160)) → new_primPlusInt5(xx113, xx114, xx1150, xx1160)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_rangeSize1(xx53, xx54, Succ(xx550), Succ(xx560)) → new_rangeSize1(xx53, xx54, xx550, xx560)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_rangeSize1(xx53, xx54, Succ(xx550), Succ(xx560)) → new_rangeSize1(xx53, xx54, xx550, xx560)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusInt6(xx108, xx109, Succ(xx1100), Succ(xx1110)) → new_primPlusInt6(xx108, xx109, xx1100, xx1110)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusInt6(xx108, xx109, Succ(xx1100), Succ(xx1110)) → new_primPlusInt6(xx108, xx109, xx1100, xx1110)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_rangeSize10(xx45, xx46, Succ(xx470), Succ(xx480)) → new_rangeSize10(xx45, xx46, xx470, xx480)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_rangeSize10(xx45, xx46, Succ(xx470), Succ(xx480)) → new_rangeSize10(xx45, xx46, xx470, xx480)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4